\begin{tabbing}
$\forall$${\it es}$:ES, $x$, $i$:Id, $T$:Type.
\\[0ex]($\forall$$x$, $y$:$T$. Dec($x$ $=$ $y$ $\in$ $T$))
\\[0ex]$\Rightarrow$ vartype($i$;$x$) $\subseteq\rho$ $T$
\\[0ex]$\Rightarrow$ (\=$\forall$${\it e'}$, $e$:E.\+
\\[0ex]$e$ $\leq$ ${\it e'}$ 
\\[0ex]$\Rightarrow$ loc(${\it e'}$) $=$ $i$
\\[0ex]$\Rightarrow$ $\neg$($x$ after ${\it e'}$) $=$ ($x$ when $e$) $\in$ $T$
\\[0ex]$\Rightarrow$ ($\exists$${\it ev}$:E. $e$ $\leq$ ${\it ev}$  \& ${\it ev}$ $\leq$ ${\it e'}$  \& $\neg$($x$ after ${\it ev}$) $=$ ($x$ when ${\it ev}$) $\in$ $T$))
\-
\end{tabbing}